feat(invariant): assert all invariants by default (assert_all)#12587
feat(invariant): assert all invariants by default (assert_all)#12587
assert_all)#12587Conversation
1ab125d to
a398def
Compare
continuous_run
Not to say this can't be done, but this isn't how Medusa/Echidna do it. The "pro" that comes to mind is you may find a smaller reproducer or a reproducer that reveals the patch was incomplete i.e. only fixed one repro but not the other. It is possible to do deduplication with the edge map to avoid saving too many if you went this route. |
I see, makes sense, can accommodate such |
|
This looks great. Some quick ideas for further improvements:
|
| /// Display counterexample as solidity calls. | ||
| pub show_solidity: bool, | ||
| /// Continue invariant run until all invariants declared in current test suite breaks. | ||
| pub continuous_run: bool, |
There was a problem hiding this comment.
not sure if this term was chosen for a specific reason, but i was thinking this could be --no-fail-fast like for cargo?
edit: i see we have --fail-fast on forge test, i guess we can't really make a --no-fail-fast as these would seem linked and the current default is actually --no-fail-fast (for the entire suite)
This comment was marked as spam.
This comment was marked as spam.
feat(invariant): assert all invariants on continuous_run (merge upstream foundry-rs#12587)
98b7cda to
a6667e3
Compare
continuous_runassert_all)
Renames the InvariantConfig field to better describe its semantics
("assert every invariant in the suite, don't stop on first failure")
and flips the default to true so multi-invariant suites report all
broken invariants by default, matching Echidna/Medusa behavior.
Co-authored-by: Amp <amp@ampcode.com>
Amp-Thread-ID: https://ampcode.com/threads/T-019dcd68-66ac-76ed-ac5c-7ea722a9c9ae
d4aa568 to
b012dbd
Compare
…d failures footer - Generalize shrink_sequence, shrink_sequence_value, replay_run, replay_error to accept target_invariant: &Function (currently always primary; unblocks per-secondary shrinking). - Move reset_shrink_progress out of shrink fns; called once per invariant from replay_error. Progress label now 'Shrink: <invariant_name>'. - Add TestResult.invariant_failure_dir; Display appends 'N invariant failures persisted to <dir> — rerun to shrink' when secondary failures were written. Amp-Thread-ID: https://ampcode.com/threads/T-019dcd68-66ac-76ed-ac5c-7ea722a9c9ae Co-authored-by: Amp <amp@ampcode.com>
…ndaries Promotes TestResult.other_failures from Vec<String> to Vec<InvariantOtherFailure> carrying name, reason, optional counterexample, and persisted path. Display renders each secondary symmetrically with [FAIL: reason] + [Sequence] block when a counterexample is available, falling back to the terse 'name: reason' one-liner otherwise. Amp-Thread-ID: https://ampcode.com/threads/T-019dcd68-66ac-76ed-ac5c-7ea722a9c9ae Co-authored-by: Amp <amp@ampcode.com>
…nk secondaries PR-3 of the assert_all rollout. After the campaign finishes, every broken secondary invariant is shrunk in turn via replay_error so users get a ready-to-debug counterexample for each failure in a single run (matching how the primary is rendered: [FAIL: reason] <name> + [Sequence] block). On Ctrl-C, instead of dropping known secondaries (previous behavior was a 'break' before pushing them), the loop keeps recording every failure the campaign discovered. The shrink + replay step is skipped to honor the interrupt, but the un-shrunk sequence is persisted via BaseCounterExample::from_invariant_call (no execution required), so a re-run targeting that secondary picks up the saved counterexample and shrinks from there — same UX as re-running an interrupted primary. Output of an interrupted run now includes a terse '<invariant>: <reason>' line for each secondary the campaign saw, preserving visibility of all broken invariants while keeping the interrupt fast. Adds e2e coverage: - assert_all: extended to verify secondary failures render symmetrically with shrunk sequences and that re-running skips persisted secondaries. - assert_all_only_primary: new test confirming no secondary [FAIL] blocks or persisted-failures footer appear when only the primary breaks. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dcdd3-53f5-76b6-ac36-d59f06b58280
…-up, opt-mode warning Three small UX wins for assert_all campaigns. No behavior change, no new dependencies. 1. Shrink progress bar gets an [i/N] queue counter when more than one invariant needs shrinking, so users see how many shrinkers are queued behind the current one (e.g. '[2/3] Shrink: invariant_X'). reset_shrink_progress and replay_error gain a position parameter; single-invariant call sites pass None. 2. Suite-level roll-up footer: when assert_all exercised >1 invariant and the test failed, render 'Suite assert_all: <broken>/<total> invariants broken' above the per-invariant blocks. Gives CI logs and Slack pastes a glanceable health line. New Option<usize> field on TestResult, populated only when meaningful. 3. Startup warning when assert_all + optimization-mode are combined. Optimization mode tracks one int256 return value, so any boolean secondary invariants in the same contract are filtered out before the campaign — previously silent. Now emits a once-per-suite warning naming the optimization invariant and every dropped boolean so users can move them to a separate contract. E2E tests: extend assert_all to assert the new 4/5 roll-up; assert_all_only_primary covers the 1/2 case; new assert_all_optimization_mode_warning verifies the warning fires with the dropped invariant names. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dcdd3-53f5-76b6-ac36-d59f06b58280
… failures Symmetric with the primary's existing persisted-replay warning. Echidna and Medusa never silently drop properties between runs — properties are re-evaluated every campaign and a previous failure doesn't suppress them. Foundry's per-property failure file model meant secondaries with a stale persisted counterexample were filtered out of the campaign with no acknowledgment, so users coming from Echidna/Medusa would see fewer invariants in the report than their contract defines. Now emits one stderr line listing every skipped name and the cache dir to clean, e.g.: Warning: test/X.t.sol:Suite: 3 invariant(s) skipped due to persisted failures: invariant_a, invariant_b, invariant_c. Run `forge clean` or delete files in cache/invariant/failures/Suite to re-include. E2E: extends assert_all re-run case with stderr_eq snapshot asserting the warning fires with all 3 skipped names. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dcdd3-53f5-76b6-ac36-d59f06b58280
Previously afterInvariant was gated on failures.errors.is_empty() campaign-wide. Under assert_all that gate stayed closed for the rest of the campaign once any invariant broke, silently skipping the afterInvariant hook on every subsequent run. Any assertions or cleanup logic in afterInvariant therefore stopped running after the first unrelated invariant failure. Now snapshot failures.errors.len() at the start of each run and only skip afterInvariant when the current run produced a new failure. Preserves the legacy 'don't run afterInvariant on a run that already failed' semantics while letting it run on subsequent runs once an earlier invariant has broken. E2E: new assert_all_after_invariant_runs_after_earlier_failure case breaks invariant_first in run 1, keeps the campaign alive with a second never-breaking invariant, and asserts an always-reverting afterInvariant surfaces its marker in failure output. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dce2d-57c7-734a-bbc6-6fa5e34b25de
3b61e25 to
8f34444
Compare
…change The secondary persisted-failure skip used a bare `.exists()` check at two sites in runner.rs (the warning + InvariantContract::new filter, and the post-campaign shrink loop). Under the new `assert_all = true` default this meant any leftover failure file from a previous run was treated as still valid even after the user changed a tracked setting (target contracts/selectors, target/excluded senders, fail_on_revert), silently dropping the secondary from the campaign with a misleading 'skipped due to persisted failures' warning. Now both sites use the same settings-aware compatibility check the primary's replay path uses (persisted_call_sequence settings.diff). Stale caches fall back to a fresh evaluation; only secondaries whose persisted settings still match the current run are honored. Also hoists current_settings up so the new secondary_has_compatible_persisted closure can reuse it across all three call sites (warning, filter, shrink-loop skip). E2E: new assert_all_secondary_persisted_revalidates_on_settings_change runs once with fail_on_revert=false, flips it to true, re-runs and asserts the suite roll-up shows 2/2 invariants broken — proving the secondary was re-evaluated rather than silently filtered out. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dce2d-57c7-734a-bbc6-6fa5e34b25de
…assert_all When the selected invariant test passes but a secondary breaks under assert_all, the report previously rendered a hollow '[FAIL]' header (no reason, no counterexample) for the primary and the suite roll-up overcounted broken invariants as '1 + other_failures.len()', attributing a non-existent primary failure. Now key the primary header on whether the primary actually broke (`reason.is_some() || counterexample.is_some()`) and skip the header when it didn't. Roll-up uses the same flag so the count reflects only invariants that actually broke (e.g., 1/2 instead of 2/2). JSON shape is unchanged: top-level reason/counterexample stay null when the selected primary didn't break, with full secondary detail in other_failures. E2E: new assert_all_secondary_only_failure_no_hollow_fail asserts a secondary-only break renders 'Suite assert_all: 1/2 invariants broken' followed by the secondary's '[FAIL: ...] <name>' block, with no hollow primary header. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dce2d-57c7-734a-bbc6-6fa5e34b25de
…ry-only case Previous commit suppressed the '[FAIL]' header whenever the primary had no top-level reason or counterexample, which also matches DS-style failures (they signal via the 'failed' flag and log events rather than through TestResult.reason). That regressed failure_assertions::ds_style_test_failing and test_cmd::core::legacy_assertions in CI. Now the suppression is scoped strictly to the assert_all secondary-only case: skip the primary header only when no primary failure AND assert_all is in play AND there is at least one secondary to render. DS-style, plain unit and single-invariant failures keep the original '[FAIL]'/'[FAIL: ...]' rendering. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dce2d-57c7-734a-bbc6-6fa5e34b25de
…declaration order The structured JSON 'failure' event emitted to stderr at campaign end (consumed by benchmark and CI tooling) used 'errors.values().next()' on a HashMap to pick its 'reason' field, while hardcoding the 'invariant' field to the primary's name. With HashMap RandomState, the same broken set of invariants produced a different reason string across runs, and the event was self-inconsistent (e.g., 'invariant: invariant_balance, reason: fee miscalculation'). Three sites used this pattern: in-run break path, afterInvariant break path, and the preflight check fallback. Now they walk 'invariant_contract.invariant_fns' in declaration order (a Vec, deterministic) and pick the first one with a recorded failure. Both 'invariant' and 'reason' fields refer to the same function, and the event is stable across runs. A new 'first_broken_event' helper centralizes the lookup. E2E: assert_all_failure_event_uses_declaration_order declares three invariants (a, b, c) that all break on the same call, runs with '--mt invariant_c' (primary is the last declared) and asserts the emitted event names invariant_a with reason 'a broken'. Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019dce2d-57c7-734a-bbc6-6fa5e34b25de
…secondary_failures and serialize sparsely
Renames TestResult.other_failures -> invariant_secondary_failures and
the underlying InvariantOtherFailure struct -> InvariantSecondaryFailure.
The previous names were generic ('other relative to what?'); the new
names align with the existing 'primary/secondary' terminology used
throughout the assert_all rollout and follow the Rust Vec<Foo>/foos
plural-of-singular convention.
Also marks the field with #[serde(default, skip_serializing_if =
'Vec::is_empty')] so it is omitted from JSON output for any test that
has no secondary failure data — plain unit tests, fuzz tests, passing
tests. Pre-PR JSON consumers continue to see the same shape on those
results. invariant_failure_dir and assert_all_invariant_count already
had Option::is_none guards.
Updates the SimpleContractTest{NonVerbose,Verbose}.json fixtures to
drop the now-skipped empty field.
Co-authored-by: Amp <amp@ampcode.com>
Amp-Thread-ID: https://ampcode.com/threads/T-019dce2d-57c7-734a-bbc6-6fa5e34b25de
e2746b2 to
eb51a9d
Compare
| calldata, | ||
| call_result, | ||
| &inner_sequence, | ||
| if invariant_failures.has_failure(invariant) { |
There was a problem hiding this comment.
Given this is mut (invariant_failures: &mut InvariantFailures,), couldn't we remove failing invariant_fn and avoid this lookup? Only other reason to keep it around would be to store duplicate failures, but we're not doing that here
There was a problem hiding this comment.
yep, good point. I evaluated the change and it's a bigger refactor, OK if will do in a follow-up / cleanup?
There was a problem hiding this comment.
Tbh I think it is fine to just keep calling these, and we should figure out a deduplication strategy. #14482 (comment)
There was a problem hiding this comment.
kk, will follow up on #14482 with dedup strategy
…) to all live invariants Amp-Thread-ID: https://ampcode.com/threads/T-019dd262-ed81-723c-aaaa-8e1314bed45a Co-authored-by: Amp <amp@ampcode.com>
closes #9727
Adds
invariant.assert_all(defaulttrue, matches Echidna/Medusa). When enabled the campaign keeps running after the first broken invariant and shrinks every broken one in a single run.What this PR adds:
[FAIL: reason] <name>+[Sequence]block for each broken invariantSuite assert_all: <broken>/<total> invariants brokenroll-up above the per-invariant blocks[i/N] Shrink: <invariant>counter on the progress bar when more than one invariant needs shrinkingN invariant failures persisted to <dir> — rerun to shrinkfooterassert_all + optimization invariant(boolean secondaries silently filtered) andN invariant(s) skipped due to persisted failureson re-runsinvariant.assert_all = falseto restore the legacy "stop on first broken invariant" behavior@forkforkdog @rappie @GalloDaSballo appreciate some feedback and if that's what you were looking for, thank you
CC @0xalpharush
PR Checklist